\begin{tabbing}
R{-}consistent($R$; ${\it es}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$es\_realizer\_ind(\=$R$;\+
\\[0ex]True;
\\[0ex]${\it left}$,${\it right}$,${\it rec}_{1}$,${\it rec}_{2}$.(${\it rec}_{1}$ $\wedge$ ${\it rec}_{2}$);
\\[0ex]$i$,$T$,$x$,$V$.case $V$
\\[0ex]o\=f inl($v$) =$>$ init{-}p(${\it es}$; $i$; $T$; $x$; $v$)\+
\\[0ex]$\mid$ inr($v$) =$>$ init\_p(${\it es}$; $i$; $T$; $x$; $v$);
\-\\[0ex]$i$,$T$,$x$,$L$.frame{-}p(${\it es}$; $i$; $T$; $x$; $L$);
\\[0ex]$l$,${\it tg}$,$L$.sframe{-}p(${\it es}$; $l$; ${\it tg}$; $L$);
\\[0ex]$i$,${\it ds}$,$k$,$T$,$x$,$F$.case $F$
\\[0ex]o\=f inl($f$) =$>$ effect{-}p(${\it es}$; $i$; ${\it ds}$; $k$; $T$; $x$; $f$)\+
\\[0ex]$\mid$ inr($f$) =$>$ effect\_p(${\it es}$; $i$; ${\it ds}$; $k$; $T$; $x$; $f$);
\-\\[0ex]${\it ds}$,$k$,$T$,$l$,${\it dt}$,$g$.sends{-}p(${\it es}$; ${\it ds}$; $k$; $T$; $l$; ${\it dt}$; $g$);
\\[0ex]$i$,${\it ds}$,$a$,${\it prob}$,$P$.pre{-}p(${\it es}$; $i$; ${\it ds}$; $a$; ${\it prob}$; $P$);
\\[0ex]$i$,$k$,$L$.aframe{-}p(${\it es}$; $i$; $k$; $L$);
\\[0ex]$i$,$k$,$L$.bframe{-}p(${\it es}$; $i$; $k$; $L$);
\\[0ex]$i$,$x$,$L$.rframe{-}p(${\it es}$; $i$; $x$; $L$))
\-
\end{tabbing}